es{-}state{-}after{-}elapsed(${\it es}$; $e$; $t$)($x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$es\_state\_after(${\it es}$; $e$)($x$,$t$)